\documentclass[a4paper,10pt]{article}
\usepackage[utf8x]{inputenc}
\usepackage[polish]{babel}
\usepackage[T1]{fontenc}
\usepackage[dvips]{graphicx}
\usepackage{latexsym}
\usepackage{amsmath}

\makeatletter
\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
  {-3.25ex\@plus -1ex \@minus -.2ex}%
  {1.5ex \@plus .2ex}%
  {\normalfont\normalsize\bfseries}}
\makeatother

%opening
\title{Zadanie Zaliczeniowe}
\author{Kacper Chwiałkowski}

\begin{document}

\maketitle

\begin{abstract}

\end{abstract}

\section{Składnia}

\subsection{Gramatyka}

\paragraph{Produkcje}

\begin{verbatim}
Rule 0     S' -> statement
Rule 1     statement -> formula
Rule 2     statement -> formula DEF formula
Rule 3     formula -> formula AND formula
Rule 4     formula -> formula OR formula
Rule 5     formula -> formula THEN formula
Rule 6     formula -> NOT formula
Rule 7     formula -> LPAREN formula RPAREN
Rule 8     formula -> relation
Rule 9     relation -> CONST
Rule 10    relation -> CONST LPAREN listargs RPAREN
Rule 11    listargs -> term
Rule 12    listargs -> term COMMA listargs
Rule 13    term -> VAR
Rule 14    term -> relation
\end{verbatim}

\paragraph{Mapowanie symboli}

\begin{verbatim}
AND                  : &&
COMMA                : ,
CONST                : r'[A-Z][a-zA-Z0-9_]*'
DEF                  : =>
LPAREN               : (
NEWLINE              : \n
NOT                  : ~
OR                   : ||
RPAREN               : )
THEN                 : ->
VAR                  : r'[a-z][a-zA-Z0-9_]*'
\end{verbatim}


\paragraph{Znaczenie ważniejszych symboli}


\begin{itemize}
 \item[AND] - koniunkcja
 \item[CONST] - nazwa relacji
 \item[DEF] - definiuje regułe wnioskowania postaci \[ \frac{A(x) : B(x)}{ B(x)} \] 
 \item[OR ] - altrenatywa
 \item[THEN] - implikacja
 \item[NOT] - zaprzeczenie
 \item[VAR] - zmienna
\end{itemize}


\paragraph{Przykładowy program tłumaczenie}

\begin{itemize}
 
\item Najmocniej wiąże ~, potem kolejno ->, \&\& i ||

\begin{verbatim}
 C && A && B || C -> ~D
\end{verbatim}

\[ (( C \wedge (A \wedge B)) \vee C) -> ~D \] 


\item Tłumaczenie ``Dla Każdego''. Zakłada się że jesli w formule istnieja wolne zmienne do przed formuła jest 
dla każdego.
\begin{verbatim}
S(S(y,x)) 
\end{verbatim}

\[ \forall x \forall y S(S(x,y)) \]

\item Tłumaczenie domniemań
\begin{verbatim}
 S(x,z,N) -> K(z,x) => Z(x)
\end{verbatim}

\[  \frac{ \forall z ( S(x,z,N) -> K(z,x) ) : Z(x)}{ Z(x)} \] 

\end{itemize}

\paragraph{Implementacja}
Parser znajduje się w pliku parser.py w katalogu syntax. Został napisany w pythonie przy pomocy 
biblioteki PLY.

\end{document}
